n:, f:(n), m, k:n.
m = k    (x:n. x = m    x = k    f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k) 

latex

Definitions	i  j < k, AB, P & Q, False, sum(f(x) | x < k), P  Q, x(s), A, Prop, {i..j}, x:A. B(x), t  T, , if b t else f fi, i=j, Unit, P  Q, , b, b
Lemmas	assert wf, bnot wf, bool wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, eq int wf, ifthenelse wf, singleton support sum, isolate summand, nat wf, int seg wf, not wf